$\forall$${\it es}$:ES, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$, ${\it e'}$:E. Dec($R$(${\it e'}$,$e$)))
\\[0ex]$\Rightarrow$ $R$ =$>$ $\lambda$$x$,$y$. ($x$ $<$ $y$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($\exists$${\it e'}$:E. ($R$(${\it e'}$,$e$))) $\Rightarrow$ ($\exists$${\it e'}$:E. es{-}r{-}immediate{-}pred(${\it es}$;$R$;${\it e'}$;$e$)))